#ifndef CKT_Cover_H
#define CKT_Cover_H

#include "rewrite/isop.h"
#include "info/icut.h"
#include <cstring>

struct BestCut;
struct SATSolver;
struct Lit;
typedef Lit lit_t;

class Cover
{
   public:
   virtual ~Cover(){}

   virtual unsigned ncls()=0;
   virtual unsigned area()=0;
   virtual void dumpClause( unsigned , lit_t * , SATSolver & , uint8_t ph)=0;
   
   virtual unsigned size()const=0;
   virtual unsigned at( unsigned i )const=0;
};
class CutCover : public Cover , public Cut 
{
   unsigned sz;
   
   public:
   CutCover(unsigned short s , const Cut & c );
   virtual ~CutCover(){}
   
   virtual void dumpClause( unsigned , lit_t * , SATSolver & , uint8_t ph);
   virtual unsigned ncls();
   virtual unsigned area();
   
   virtual unsigned size()const{ return sz ;}
   virtual unsigned at( unsigned i ) const{ return node[i];}
};
class ANDCover : public Cover 
{
   unsigned sign:1;
   unsigned sz:31;
   AigLit * dat;
   public:
   ANDCover( unsigned s , unsigned * d , unsigned sg )
      :sign(sg),sz(s)
   { 
      dat=new AigLit [sz] ; 
      memcpy( dat , d , sizeof( AigLit )*sz );
   }
   virtual ~ANDCover(){ delete [] dat; }
  
   virtual void dumpClause( unsigned , lit_t * , SATSolver & , uint8_t ph );
   virtual unsigned ncls(){ return sz+1;}
   virtual unsigned area(){ return sz*3+1;}

   virtual unsigned size()const{return sz;}
   virtual unsigned at( unsigned i ) const {return var( dat[i]);}
};
class CktCover : public InfoCut , ISOP
{
   // COVERING FUNCTIONS 
   //
   void dp_covering();
   void dp_covering(BestCut * );
   void dp_compute( unsigned short * refcnt , BestCut * );
   void dp_refine( BestCut * , unsigned short * refcnt);

   void bigAnd_covering();
   bool bigAnd_covering( unsigned n );
   bool isCut_an_and( unsigned , vec<AigLit> & fanin, uint8_t & );

   unsigned deactivate( unsigned n , unsigned lim , vec<unsigned> & );
   void deactivate( unsigned n );
   int  activate( Cover * , int );
   void deactivate( vec<unsigned> & );
   bool change( unsigned n , Cover * c );
   void optimize();

   Cover **  _cover;    ///< the cover, if focnt not 0 the cover is activate
   uint8_t * _satph;    ///< the phase of the node( use in dump cnf ) , setted by init( arg )
   unsigned  _nvar;     ///< number of variable

   public:
   lit_t   *   _lits;   ///< assigned literal
   CktCover();
   ~CktCover();

   void init(bool );
   void covering();

   void write_cnf( const char * file );///< assign all po 0

   // REPORTING FUNCTION
   //
   void report_covering()const;
   unsigned nClause()const;
   unsigned nVars()const{return _nvar ;}
   Lit getLit( AigLit x )const;

   // ASSIGN SOLVER
   //
   void assignLit( int v = 0 );
   void assignCNF(   SATSolver & s );
   void assignCNFPO( SATSolver & s ); // use in sat 
   void const_propagation();
};

#endif
